I uncommented the new instructions, generated the tests (just tried mp for now) and I was able to run them with no problem with the code from hernanponcedeleon/Dat3M#985.

However, the results using cpp2w.cat do not yet match the naming convention, e.g., here are two example outputs

Test: tests/mp/mp-sna-frel-saddrlx-lrlx-facq-faddrlx.undef.litmus
Result: PASS
Time: 0.039 secs

Test: tests/mp/mp-srlx-saddrel-srlx-lrlx-lacq-lna.undef.litmus
Result: FAIL
Reason: CAT specification violation found
Details:
	Flag Dr (*undef*)
	E3 / E16	@unknown / @unknown
Time: 0.039 secs

I also do not understand the difference between racy and undef in the naming.

Thanks I'll check it out with that code.

I also do not understand the difference between racy and undef in the naming.

There are two things I wanted to test:

• undef: a test that should have an undefined behavior outcome does have it (data-race is not empty, e.g., a test that should have access some location with atomics, accidentally accessed it with non-atomic operations).
• racy: a test that should not have undefined behavior but is not properly synchronized, does not have undefined behavior, and all permitted results can be observed (e.g. a test that uses relaxed atomics, but forgot some fences)

Using undef and racy in the file names was just an easy way of using grep to check the presence/absence of undefined behavior / data-race-is-empty in the tool output (e.g. herd prints or does not print Undef).

I hope there is a better way to do this.